Termination w.r.t. Q of the following Term Rewriting System could not be shown:
Q restricted rewrite system:
The TRS R consists of the following rules:
a2(f, 0) -> a2(s, 0)
a2(d, 0) -> 0
a2(d, a2(s, x)) -> a2(s, a2(s, a2(d, a2(p, a2(s, x)))))
a2(f, a2(s, x)) -> a2(d, a2(f, a2(p, a2(s, x))))
a2(p, a2(s, x)) -> x
Q is empty.
↳ QTRS
↳ Non-Overlap Check
Q restricted rewrite system:
The TRS R consists of the following rules:
a2(f, 0) -> a2(s, 0)
a2(d, 0) -> 0
a2(d, a2(s, x)) -> a2(s, a2(s, a2(d, a2(p, a2(s, x)))))
a2(f, a2(s, x)) -> a2(d, a2(f, a2(p, a2(s, x))))
a2(p, a2(s, x)) -> x
Q is empty.
The TRS is non-overlapping. Hence, we can switch to innermost.
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
a2(f, 0) -> a2(s, 0)
a2(d, 0) -> 0
a2(d, a2(s, x)) -> a2(s, a2(s, a2(d, a2(p, a2(s, x)))))
a2(f, a2(s, x)) -> a2(d, a2(f, a2(p, a2(s, x))))
a2(p, a2(s, x)) -> x
The set Q consists of the following terms:
a2(f, 0)
a2(d, 0)
a2(d, a2(s, x0))
a2(f, a2(s, x0))
a2(p, a2(s, x0))
Q DP problem:
The TRS P consists of the following rules:
A2(f, a2(s, x)) -> A2(p, a2(s, x))
A2(f, a2(s, x)) -> A2(d, a2(f, a2(p, a2(s, x))))
A2(d, a2(s, x)) -> A2(d, a2(p, a2(s, x)))
A2(d, a2(s, x)) -> A2(s, a2(d, a2(p, a2(s, x))))
A2(d, a2(s, x)) -> A2(s, a2(s, a2(d, a2(p, a2(s, x)))))
A2(f, a2(s, x)) -> A2(f, a2(p, a2(s, x)))
A2(f, 0) -> A2(s, 0)
A2(d, a2(s, x)) -> A2(p, a2(s, x))
The TRS R consists of the following rules:
a2(f, 0) -> a2(s, 0)
a2(d, 0) -> 0
a2(d, a2(s, x)) -> a2(s, a2(s, a2(d, a2(p, a2(s, x)))))
a2(f, a2(s, x)) -> a2(d, a2(f, a2(p, a2(s, x))))
a2(p, a2(s, x)) -> x
The set Q consists of the following terms:
a2(f, 0)
a2(d, 0)
a2(d, a2(s, x0))
a2(f, a2(s, x0))
a2(p, a2(s, x0))
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A2(f, a2(s, x)) -> A2(p, a2(s, x))
A2(f, a2(s, x)) -> A2(d, a2(f, a2(p, a2(s, x))))
A2(d, a2(s, x)) -> A2(d, a2(p, a2(s, x)))
A2(d, a2(s, x)) -> A2(s, a2(d, a2(p, a2(s, x))))
A2(d, a2(s, x)) -> A2(s, a2(s, a2(d, a2(p, a2(s, x)))))
A2(f, a2(s, x)) -> A2(f, a2(p, a2(s, x)))
A2(f, 0) -> A2(s, 0)
A2(d, a2(s, x)) -> A2(p, a2(s, x))
The TRS R consists of the following rules:
a2(f, 0) -> a2(s, 0)
a2(d, 0) -> 0
a2(d, a2(s, x)) -> a2(s, a2(s, a2(d, a2(p, a2(s, x)))))
a2(f, a2(s, x)) -> a2(d, a2(f, a2(p, a2(s, x))))
a2(p, a2(s, x)) -> x
The set Q consists of the following terms:
a2(f, 0)
a2(d, 0)
a2(d, a2(s, x0))
a2(f, a2(s, x0))
a2(p, a2(s, x0))
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 2 SCCs with 6 less nodes.
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
A2(d, a2(s, x)) -> A2(d, a2(p, a2(s, x)))
The TRS R consists of the following rules:
a2(f, 0) -> a2(s, 0)
a2(d, 0) -> 0
a2(d, a2(s, x)) -> a2(s, a2(s, a2(d, a2(p, a2(s, x)))))
a2(f, a2(s, x)) -> a2(d, a2(f, a2(p, a2(s, x))))
a2(p, a2(s, x)) -> x
The set Q consists of the following terms:
a2(f, 0)
a2(d, 0)
a2(d, a2(s, x0))
a2(f, a2(s, x0))
a2(p, a2(s, x0))
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
A2(f, a2(s, x)) -> A2(f, a2(p, a2(s, x)))
The TRS R consists of the following rules:
a2(f, 0) -> a2(s, 0)
a2(d, 0) -> 0
a2(d, a2(s, x)) -> a2(s, a2(s, a2(d, a2(p, a2(s, x)))))
a2(f, a2(s, x)) -> a2(d, a2(f, a2(p, a2(s, x))))
a2(p, a2(s, x)) -> x
The set Q consists of the following terms:
a2(f, 0)
a2(d, 0)
a2(d, a2(s, x0))
a2(f, a2(s, x0))
a2(p, a2(s, x0))
We have to consider all minimal (P,Q,R)-chains.